{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (nameTxCert) where import Cardano.Ledger.Conway import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..)) import Constrained.API import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert) import Test.Cardano.Ledger.Constrained.Conway import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse instance ExecSpecRule "CERT" ConwayEra where type ExecContext "CERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) genExecContext :: HasCallStack => Gen (ExecContext "CERT" 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 "CERT" ConwayEra -> Specification (ExecEnvironment "CERT" ConwayEra) environmentSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra _) = forall era. EraSpecPParams era => WitUniv era -> Specification (CertEnv era) certEnvSpec @ConwayEra WitUniv ConwayEra univ stateSpec :: HasCallStack => ExecContext "CERT" ConwayEra -> ExecEnvironment "CERT" ConwayEra -> Specification (ExecState "CERT" ConwayEra) stateSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra ccec) ExecEnvironment "CERT" ConwayEra _ = 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 "CERT" ConwayEra -> ExecEnvironment "CERT" ConwayEra -> ExecState "CERT" ConwayEra -> Specification (ExecSignal "CERT" ConwayEra) signalSpec (WitUniv ConwayEra univ, ConwayCertExecContext ConwayEra _) ExecEnvironment "CERT" ConwayEra env ExecState "CERT" ConwayEra state = forall era. (era ~ ConwayEra) => WitUniv era -> CertEnv era -> CertState era -> Specification (ConwayTxCert era) conwayTxCertSpec @ConwayEra WitUniv ConwayEra univ ExecEnvironment "CERT" ConwayEra env ExecState "CERT" ConwayEra state runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "CERT" ConwayEra) -> SpecRep (ExecState "CERT" ConwayEra) -> SpecRep (ExecSignal "CERT" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "CERT" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "CERT" ConwayEra) env SpecRep (ExecState "CERT" ConwayEra) st SpecRep (ExecSignal "CERT" ConwayEra) sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a unComputationResult forall a b. (a -> b) -> a -> b $ CertEnv -> CertState -> DCert -> T_ComputationResult_46 Text CertState Agda.certStep SpecRep (ExecEnvironment "CERT" ConwayEra) env SpecRep (ExecState "CERT" ConwayEra) st SpecRep (ExecSignal "CERT" ConwayEra) sig classOf :: ExecSignal "CERT" ConwayEra -> Maybe String classOf = forall a. a -> Maybe a Just forall b c a. (b -> c) -> (a -> b) -> a -> c . ConwayTxCert ConwayEra -> String nameTxCert nameTxCert :: ConwayTxCert ConwayEra -> String nameTxCert :: ConwayTxCert ConwayEra -> String nameTxCert (ConwayTxCertDeleg ConwayDelegCert x) = ConwayDelegCert -> String nameDelegCert ConwayDelegCert x nameTxCert (ConwayTxCertPool PoolCert x) = PoolCert -> String namePoolCert PoolCert x nameTxCert (ConwayTxCertGov ConwayGovCert x) = ConwayGovCert -> String nameGovCert ConwayGovCert x