{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert) where import Cardano.Ledger.Address (RewardAccount) import Cardano.Ledger.BaseTypes (Inject (..)) import Cardano.Ledger.Coin (Coin) import Cardano.Ledger.Conway import Cardano.Ledger.Conway.Governance (VotingProcedures) import Cardano.Ledger.Conway.TxCert import Constrained.API import Data.Bifunctor (Bifunctor (..)) import Data.Map.Strict (Map) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ( ConwayCertExecContext (..), conwayCertExecContextSpec, ) import Test.Cardano.Ledger.Constrained.Conway import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map RewardAccount Coin) where inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) -> Map RewardAccount Coin inject (WitUniv ConwayEra _, ConwayCertExecContext ConwayEra x) = forall era. ConwayCertExecContext era -> Map RewardAccount Coin ccecWithdrawals ConwayCertExecContext ConwayEra x instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) where inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) -> VotingProcedures ConwayEra inject (WitUniv ConwayEra _, ConwayCertExecContext ConwayEra x) = forall era. ConwayCertExecContext era -> VotingProcedures era ccecVotes ConwayCertExecContext ConwayEra x instance ExecSpecRule "GOVCERT" ConwayEra where type ExecContext "GOVCERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) genExecContext :: HasCallStack => Gen (ExecContext "GOVCERT" ConwayEra) genExecContext = do WitUniv ConwayEra univ <- forall era. (GenScript era, HasWitness ScriptHash era) => Int -> Gen (WitUniv era) genWitUniv @ConwayEra Int 300 ConwayCertExecContext ConwayEra ccec <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a genFromSpec (forall era. Era era => WitUniv era -> Integer -> Specification (ConwayCertExecContext era) conwayCertExecContextSpec WitUniv ConwayEra univ Integer 5) forall (f :: * -> *) a. Applicative f => a -> f a pure (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra ccec) environmentSpec :: HasCallStack => ExecContext "GOVCERT" ConwayEra -> Specification (ExecEnvironment "GOVCERT" ConwayEra) environmentSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra _) = WitUniv ConwayEra -> Specification (ConwayGovCertEnv ConwayEra) govCertEnvSpec WitUniv ConwayEra univ stateSpec :: HasCallStack => ExecContext "GOVCERT" ConwayEra -> ExecEnvironment "GOVCERT" ConwayEra -> Specification (ExecState "GOVCERT" ConwayEra) stateSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra ccec) ExecEnvironment "GOVCERT" ConwayEra _env = forall era. EraSpecCert era => WitUniv era -> Set (Credential 'DRepRole) -> Map RewardAccount Coin -> Specification (CertState era) certStateSpec @ConwayEra WitUniv ConwayEra univ (forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole) ccecDelegatees ConwayCertExecContext ConwayEra ccec) (forall era. ConwayCertExecContext era -> Map RewardAccount Coin ccecWithdrawals ConwayCertExecContext ConwayEra ccec) signalSpec :: HasCallStack => ExecContext "GOVCERT" ConwayEra -> ExecEnvironment "GOVCERT" ConwayEra -> ExecState "GOVCERT" ConwayEra -> Specification (ExecSignal "GOVCERT" ConwayEra) signalSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra _) = forall era. EraCertState era => WitUniv era -> ConwayGovCertEnv ConwayEra -> CertState ConwayEra -> Specification ConwayGovCert govCertSpec WitUniv ConwayEra univ classOf :: ExecSignal "GOVCERT" ConwayEra -> Maybe String classOf = forall a. a -> Maybe a Just forall b c a. (b -> c) -> (a -> b) -> a -> c . ConwayGovCert -> String nameGovCert runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "GOVCERT" ConwayEra) -> SpecRep (ExecState "GOVCERT" ConwayEra) -> SpecRep (ExecSignal "GOVCERT" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "GOVCERT" ConwayEra) env (Agda.MkCertState DState dState PState pState GState vState) SpecRep (ExecSignal "GOVCERT" ConwayEra) sig = forall (p :: * -> * -> *) b c a. Bifunctor p => (b -> c) -> p a b -> p a c second (DState -> PState -> GState -> CertState Agda.MkCertState DState dState PState pState) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. ComputationResult T_String_6 a -> Either OpaqueErrorString a unComputationResult forall a b. (a -> b) -> a -> b $ CertEnv -> GState -> DCert -> T_ComputationResult_46 T_String_6 GState Agda.govCertStep SpecRep (ExecEnvironment "GOVCERT" ConwayEra) env GState vState SpecRep (ExecSignal "GOVCERT" ConwayEra) sig nameGovCert :: ConwayGovCert -> String nameGovCert :: ConwayGovCert -> String nameGovCert (ConwayRegDRep {}) = String "ConwayRegDRep" nameGovCert (ConwayUnRegDRep {}) = String "ConwayUnRegDRep" nameGovCert (ConwayUpdateDRep {}) = String "ConwayUpdateDRep" nameGovCert (ConwayAuthCommitteeHotKey {}) = String "ConwayAuthCommitteeHotKey" nameGovCert (ConwayResignCommitteeColdKey {}) = String "ConwayResignCommitteeColdKey"