{-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov () where import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Core (EraPParams (..)) import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Conway.Rules import Lens.Micro ((&), (.~), (^.)) 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.Constrained.Conway import Test.Cardano.Ledger.Conway.Arbitrary () import Test.Cardano.Ledger.Imp.Common instance NFData (SpecRep (ConwayGovPredFailure ConwayEra)) => ExecSpecRule "GOV" ConwayEra where type ExecContext "GOV" ConwayEra = EnactState ConwayEra environmentSpec :: HasCallStack => ExecContext "GOV" ConwayEra -> Specification (ExecEnvironment "GOV" ConwayEra) environmentSpec ExecContext "GOV" ConwayEra _ = Specification (GovEnv ConwayEra) govEnvSpec stateSpec :: HasCallStack => ExecContext "GOV" ConwayEra -> ExecEnvironment "GOV" ConwayEra -> Specification (ExecState "GOV" ConwayEra) stateSpec ExecContext "GOV" ConwayEra _ = GovEnv ConwayEra -> Specification (Proposals ConwayEra) govProposalsSpec signalSpec :: HasCallStack => ExecContext "GOV" ConwayEra -> ExecEnvironment "GOV" ConwayEra -> ExecState "GOV" ConwayEra -> Specification (ExecSignal "GOV" ConwayEra) signalSpec ExecContext "GOV" ConwayEra _ = GovEnv ConwayEra -> Proposals ConwayEra -> Specification (GovSignal ConwayEra) govProceduresSpec runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment "GOV" ConwayEra) -> SpecRep (ExecState "GOV" ConwayEra) -> SpecRep (ExecSignal "GOV" ConwayEra) -> Either OpaqueErrorString (SpecRep (ExecState "GOV" ConwayEra)) runAgdaRule SpecRep (ExecEnvironment "GOV" ConwayEra) env SpecRep (ExecState "GOV" ConwayEra) st SpecRep (ExecSignal "GOV" ConwayEra) sig = forall a. ComputationResult Text a -> Either OpaqueErrorString a unComputationResult forall a b. (a -> b) -> a -> b $ GovEnv -> GovState -> [Either GovVote GovProposal] -> T_ComputationResult_46 Text GovState Agda.govStep SpecRep (ExecEnvironment "GOV" ConwayEra) env SpecRep (ExecState "GOV" ConwayEra) st SpecRep (ExecSignal "GOV" ConwayEra) sig translateInputs :: HasCallStack => ExecEnvironment "GOV" ConwayEra -> ExecState "GOV" ConwayEra -> ExecSignal "GOV" ConwayEra -> ExecContext "GOV" ConwayEra -> ImpTestM ConwayEra (SpecRep (ExecEnvironment "GOV" ConwayEra), SpecRep (ExecState "GOV" ConwayEra), SpecRep (ExecSignal "GOV" ConwayEra)) translateInputs env :: ExecEnvironment "GOV" ConwayEra env@GovEnv {PParams ConwayEra gePParams :: forall era. GovEnv era -> PParams era gePParams :: PParams ConwayEra gePParams} ExecState "GOV" ConwayEra st ExecSignal "GOV" ConwayEra sig ExecContext "GOV" ConwayEra enactState = do GovEnv agdaEnv <- forall a (m :: * -> *) b. (HasCallStack, Show a, MonadIO m) => Either a b -> m b expectRight forall a b. (a -> b) -> a -> b $ forall ctx a. ctx -> SpecTransM ctx a -> Either Text a runSpecTransM EnactState ConwayEra ctx forall a b. (a -> b) -> a -> b $ forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep ExecEnvironment "GOV" ConwayEra env GovState agdaSt <- forall a (m :: * -> *) b. (HasCallStack, Show a, MonadIO m) => Either a b -> m b expectRight forall a b. (a -> b) -> a -> b $ forall ctx a. ctx -> SpecTransM ctx a -> Either Text a runSpecTransM EnactState ConwayEra ctx forall a b. (a -> b) -> a -> b $ forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep ExecState "GOV" ConwayEra st [Either GovVote GovProposal] agdaSig <- forall a (m :: * -> *) b. (HasCallStack, Show a, MonadIO m) => Either a b -> m b expectRight forall a b. (a -> b) -> a -> b $ forall ctx a. ctx -> SpecTransM ctx a -> Either Text a runSpecTransM EnactState ConwayEra ctx forall a b. (a -> b) -> a -> b $ forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep ExecSignal "GOV" ConwayEra sig forall (f :: * -> *) a. Applicative f => a -> f a pure (GovEnv agdaEnv, GovState agdaSt, [Either GovVote GovProposal] agdaSig) where ctx :: EnactState ConwayEra ctx = ExecContext "GOV" ConwayEra enactState forall a b. a -> (a -> b) -> b & forall era. Lens' (EnactState era) (GovRelation StrictMaybe era) ensPrevGovActionIdsL forall s t a b. ASetter s t a b -> b -> s -> t .~ forall era. GovRelation PRoot era -> GovRelation StrictMaybe era toPrevGovActionIds (ExecState "GOV" ConwayEra st forall s a. s -> Getting a s a -> a ^. forall era. Lens' (Proposals era) (GovRelation PRoot era) pRootsL) forall a b. a -> (a -> b) -> b & forall era. EraPParams era => Lens' (EnactState era) ProtVer ensProtVerL forall s t a b. ASetter s t a b -> b -> s -> t .~ (PParams ConwayEra gePParams forall s a. s -> Getting a s a -> a ^. forall era. EraPParams era => Lens' (PParams era) ProtVer ppProtocolVersionL)