{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) where import Cardano.Ledger.BaseTypes (Inject (..)) import Cardano.Ledger.Conway import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..)) import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.Keys (KeyRole (..)) import Constrained.API import Data.Bifunctor (second) import Data.Set (Set) 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.Conformance.ExecSpecRule.Core () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () import Test.Cardano.Ledger.Constrained.Conway import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Set (Credential 'DRepRole)) where inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) -> Set (Credential 'DRepRole) inject (WitUniv ConwayEra _, ConwayCertExecContext ConwayEra x) = forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole) ccecDelegatees ConwayCertExecContext ConwayEra x instance ExecSpecRule "DELEG" ConwayEra where type ExecContext "DELEG" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) genExecContext :: HasCallStack => Gen (ExecContext "DELEG" 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 "DELEG" ConwayEra -> Specification (ExecEnvironment "DELEG" ConwayEra) environmentSpec ExecContext "DELEG" ConwayEra _ = forall era. EraSpecPParams era => Specification (ConwayDelegEnv era) delegEnvSpec stateSpec :: HasCallStack => ExecContext "DELEG" ConwayEra -> ExecEnvironment "DELEG" ConwayEra -> Specification (ExecState "DELEG" ConwayEra) stateSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra ccec) ExecEnvironment "DELEG" 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 "DELEG" ConwayEra -> ExecEnvironment "DELEG" ConwayEra -> ExecState "DELEG" ConwayEra -> Specification (ExecSignal "DELEG" ConwayEra) signalSpec ExecContext "DELEG" ConwayEra _ = forall era. (EraPParams era, ConwayEraCertState era) => ConwayDelegEnv era -> CertState era -> Specification ConwayDelegCert conwayDelegCertSpec runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "DELEG" ConwayEra) -> SpecRep (ExecState "DELEG" ConwayEra) -> SpecRep (ExecSignal "DELEG" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "DELEG" ConwayEra) env (Agda.MkCertState DState dState PState pState GState vState) SpecRep (ExecSignal "DELEG" ConwayEra) sig = forall (p :: * -> * -> *) b c a. Bifunctor p => (b -> c) -> p a b -> p a c second (\DState dState' -> DState -> PState -> GState -> CertState Agda.MkCertState DState dState' PState pState GState vState) 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 $ DelegEnv -> DState -> DCert -> T_ComputationResult_46 T_String_6 DState Agda.delegStep SpecRep (ExecEnvironment "DELEG" ConwayEra) env DState dState SpecRep (ExecSignal "DELEG" ConwayEra) sig classOf :: ExecSignal "DELEG" ConwayEra -> Maybe String classOf = forall a. a -> Maybe a Just forall b c a. (b -> c) -> (a -> b) -> a -> c . ConwayDelegCert -> String nameDelegCert nameDelegCert :: ConwayDelegCert -> String nameDelegCert :: ConwayDelegCert -> String nameDelegCert ConwayRegCert {} = String "RegKey" nameDelegCert ConwayUnRegCert {} = String "UnRegKey" nameDelegCert ConwayDelegCert {} = String "DelegateWithKey" nameDelegCert ConwayRegDelegCert {} = String "RegK&DelegateWithKey"